\begin{tabbing}
d{-}realizes\=\{i:l\}\+
\\[0ex]($D$; ${\it es}$.$P$(${\it es}$))
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$${\it D'}$:dsys\{i:l\}.\+
\\[0ex]d{-}sub\=\{i:l\}\+
\\[0ex]($D$; ${\it D'}$)
\-\\[0ex]$\Rightarrow$ (\=$\forall$$w$:world\{i:l\}, $p$:fair{-}fifo\{i:l\}($w$).\+
\\[0ex]possible{-}world\{i:l\}(${\it D'}$; $w$) $\Rightarrow$ $P$(w{-}es\{i:l\}($w$; $p$)))
\-\-
\end{tabbing}